a:, n:. a = ((a  n) * n)+(a mod n) 

latex

Up	int 2, int 2
Definitions	t  T, x:A. B(x), a mod n, a  n, T, P  Q, P & Q, P  Q, P  Q, True, ff, if b then t else f fi , , tt, False, A, a  b  T , A  B, {...i}, Unit, , , , S  T
Lemmas	nat plus wf, assert of lt int, bnot of le int, true wf, squash wf, eqff to assert, assert of le int, eqtt to assert, iff transitivity, bnot wf, lt int wf, le wf, assert wf, bool wf, le int wf, nat plus inc int nzero, div rem sum, not functionality wrt iff, assert of bnot, assert of eq int, not wf, eq int wf, minus mono wrt eq, divide wfa, rem 2 to 1, div 2 to 1, add functionality wrt eq